Termination w.r.t. Q proof of TRS/higher-order/LifantsevEx5Sorting.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(max, 0), x) → x
app(app(max, x), 0) → x
app(app(max, app(s, x)), app(s, y)) → app(app(max, x), y)
app(app(min, 0), x) → 0
app(app(min, x), 0) → 0
app(app(min, app(s, x)), app(s, y)) → app(app(min, x), y)
app(app(app(app(insert, f), g), nil), x) → app(app(cons, x), nil)
app(app(app(app(insert, f), g), app(app(cons, h), t)), x) → app(app(cons, app(app(f, x), h)), app(app(app(app(insert, f), g), t), app(app(g, x), h)))
app(app(app(sort, f), g), nil) → nil
app(app(app(sort, f), g), app(app(cons, h), t)) → app(app(app(app(insert, f), g), app(app(app(sort, f), g), t)), h)
app(ascending_sort, l) → app(app(app(sort, min), max), l)
app(descending_sort, l) → app(app(app(sort, max), min), l)

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(max, 0), x) → x
app(app(max, x), 0) → x
app(app(max, app(s, x)), app(s, y)) → app(app(max, x), y)
app(app(min, 0), x) → 0
app(app(min, x), 0) → 0
app(app(min, app(s, x)), app(s, y)) → app(app(min, x), y)
app(app(app(app(insert, f), g), nil), x) → app(app(cons, x), nil)
app(app(app(app(insert, f), g), app(app(cons, h), t)), x) → app(app(cons, app(app(f, x), h)), app(app(app(app(insert, f), g), t), app(app(g, x), h)))
app(app(app(sort, f), g), nil) → nil
app(app(app(sort, f), g), app(app(cons, h), t)) → app(app(app(app(insert, f), g), app(app(app(sort, f), g), t)), h)
app(ascending_sort, l) → app(app(app(sort, min), max), l)
app(descending_sort, l) → app(app(app(sort, max), min), l)

Q is empty.